Nuprl Lemma : comp_id_mon_wf
13,42
postcript
pdf
T
:Type. (<o,Id> monoid on
T
)
IMonoid
latex
Up
groups
1
Definitions of Statement
(<o,Id> monoid on
T
)
Definitions
(<o,Id> monoid on
T
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
f
y
,
Assoc(
T
;
op
)
,
P
&
Q
,
Ident(
T
;
op
;
id
)
,
P
Q
,
Id{
T
}
Lemmas
identity
wf
,
compose
wf
,
btrue
wf
,
mk
imon
,
comp
assoc
,
comp
id
r
,
comp
id
l
origin
T:Type. (<o,Id> monoid on T) 
IMonoid T:Type. (<o,Id> monoid on T) IMonoid Tx:A. B(x)
Q